Nuprl Lemma : es-interface-right_wf 11,40

AB:Type, es:ES, X:AbsInterface(A + B). es-interface-right(X AbsInterface(B
latex


DefinitionsAbsInterface(A), es-interface-right(X), f o g  , x.A(x), invert-union(x), S  T, x:A.B(x), Void, x:AB(x), E, x:AB(x), left + right, Top, ES, t  T, Type
Lemmasevent system wf, top wf, es-E wf, invert-union wf, p-compose wf

origin